Contents

 PREFACE by the Earl of Halsbury      
 INTRODUCTION   
 
 MATHEMATICAL FOUNDATIONS

 1.  The morphology of prex-an essay in meta-algorithmics.  J. LASKI 
 2.  Program Schemata.  M.S. PATERSON  
 3.  Language definition and compiler validation.  J.J. FLORENTIN
 4.  Placing trees in lexicographic order.  H.I. SCOINS   


 THEOREM PROVING

 5.  A new look at mathematics and its mechanization.  B. MELTZER
 6.  Some notes on resolution strategies.  B. MELTZER   
 7.  The generalized resolution principle. J.A. ROBINSON 
 8.  Some tree-paring strategies for theorem proving.  D. LUCKHAM
 9.  Automatic theorem proving with equality substitutions and mathematical induction.  J.L. DARLINGTON   

 MACHINE LEARNING AND HEURISTIC PROGRAMMING

 10. On representations of problems of reasoning about actions. S. AMAREL 
 11. Descriptions.  E.W. ELCOCK
 12. Kalah on Atlas.  A.G. BELL  
 13. Experiments with a pleasure-seeking automaton.  J.E. DORAN 
 14. Collective behaviour and control problems.  V.I. VARSHAVSKY 

 MAN-MACHINE INTERACTION

 15. A comparison of heuristic, interactive, and unaided methods of solving a shortest-route problem.  D. MICHIE, J.G. FLEMING and
     J.V. OLDFIELD 
 16. Interactive programming at Carneige Tech.  A.H. BOND 
 17. Maintenance of large computer systems - the engineer's assistant.  M.H.J. BAYLIS     

 COGNITIVE PROCESSES: METHODS AND MODELS

 18. The syntactic analysis of English by machine.  J.P. THORNE, P. BRATLEY and H. DEWAR
 19. The adaptive memorization of sequences. H.C. LONGUET-HIGGINS and A. ORTONY

 PATTERN RECOGNITION

 20. An application of Graph Theory in pattern recognition. C.J. HILDITCH

 PROBLEM-ORIENTED LANGUAGES

 21. Some semantics for data structures.  D. PARK
 22. Writing search algorithms in functional form.  R.M. BURSTALL
 23. Assertions: programs written without specifying unneccessary order.  J.M. FOSTER
 24. The design philosophy of POP-2.  R.J. POPPLESTONE

 INDEX  

Bibliographic details

    Machine Intelligence 3
    Editor:

          Donald Michie
          Department of Machine Intelligence and Perception, University of Edinburgh

    Publisher: Edinburgh University Press, 1968

    Proceedings of the Third Annual Machine Intelligence Workshop, University of Edinburgh, September 1967.

Publisher: Edinburgh University Press

 PREFACE by Michael Swann, FRS                                        v


 MATHEMATICAL FOUNDATIONS

 1.  Program scheme equivalences and second-order logic.
     D.C. COOPER                                                      3
 2.  Programs and their proofs: an algebraic approach.
     R.M. BURSTALL and P.J. LANDIN                                   17
 3.  Towards the unique decomposition of graphs.  C.R. SNOW and
     H.I. SCOINS                                                     45


 THEOREM PROVING

 4.  Advances and problems in mechanical proof procedures.
     D. PRAWITZ                                                      59
 5.  Theorem-provers combining model elimination and resolution.
     D.W. LOVELAND
 6.  Semantic trees in automatic theorem-proving.  R. KOWALSKI
     and P.J. HAYES                                                  87
 7.  A machine-oriented logic incorporating the equality relation.
     E.E. SIBERT                                                    103
 8.  Paramodulation and theorem-proving in first-order theories
     with equality.  G. ROBINSON and L. WOS                         135
 9.  Mechanizing higher-order logic.  J.A. ROBINSON                 151


 DEDUCTIVE INFORMATION RETRIEVAL

 10. Theorem proving and information retrieval.  J.L. DARLINGTON    173
 11. Theorem proving by resolution as a basis for
     question-answering systems.  C. CORDELL GREEN                  183


 MACHINE LEARNING AND HEURISTIC PROGRAMMING

 12. Heuristic Dendral: a program for generating explanatory
     hypotheses in organic chemistry.  B. BUCHANAN, G. SUTHERLAND
     and E.A. FEIGENBAUM                                            209
 13. A chess-playing program.  J.J. SCOTT                           255
 14. Analysis of the machine chess game.  I.J. GOOD                 267
 15. PROSE - Parsing Recogniser Outputting Sentences in English.
     D.B. VIGOR, D. URQUHART and A. WILKINSON                       271
 16. The organization of interaction in collectives of automata.
     V.I. VARSHAVSKY                                                285


 COGNITIVE PROCESSES: METHODS AND MODELS

 17. Steps towards a model of word selection.  G.R. KISS            315
 18. The game of hare and hounds and the statistical study of
     literary vocabulary.  S.H. STOREY and M.A. MAYBREY             337
 19. The holophone - recent developments.  D.J. WILLSHAW and
     H.C. LONGUET-HIGGINS                                           349


 PATTERN RECOGNITION

 20. Pictorial relationships - a syntactic approach.  M.B. CLOWES   361
 21. On the construction of an efficient feature space for
     optical character recognition.  A.W.M. COOMBS                  385
 22. Linear skeletons from square cupboards.  C.J. HILDITCH         403


 PROBLEM-ORIENTED LANGUAGES

 23. Absys 1: an incremental compiler for assertions; an
     introduction.  J.M. FOSTER and E.W. ELCOCK                     423


 PRINCIPLES FOR DESIGNING INTELLIGENT ROBOTS

 24. Planning and generalisation in an automaton/environment
     system.  J.E. DORAN                                            433
 25. Freddy in toyland.  R.J. POPPLESTONE                           455
 26. Some philosophical problems from the standpoint of
     artificial intelligence.  J. McCARTHY and P.J. HAYES           463

 INDEX                                                              505

Publisher: Edinburgh University Press

Proceedings of the Fifth Annual Machine Intelligence Workshop, Edinburgh, 1969

Contents

 INTRODUCTION                                                       vii

 PROLOGUE

     Intelligent machinery. A.M. TURING [1912-1954]                   3

 MATHEMATICAL FOUNDATIONS

 1  Properties of programs and partial function logic.

    Z. MANNA and J. McCarthy                                         27

 2  Program schemes and recursive function theory.  R. MILNER        39

 3  Fixpoint induction and proofs of program properties.  D. PARK    59

 4  Formal description of program structure and semantics in first

    order logic.  R.M. BURSTALL                                      79

 5  A program machine symmetric automata theory.  P.J. LANDIN        99

 MECHANIZED REASONING

 6  A note on mechanizing higher order logic.  J.A. ROBINSON        121

 7  Transformational systems and the algebraic structure of atomic

    formulas.  J.C. REYNOLDS                                        135

 8  A note on inductive generalization.  C.D. PLOTKIN               153

 9  Power amplification for automatic theorem-provers.  B.MELTZER   165

 10 Search strategies for theorem-proving.  R.KOWALSKI              181

 11 An experiment in automatic induction.  R.J. POPPLESTONE         203

 MACHINE LEARNING AND HEURISTIC SEARCH

 12 First results on the effect of error in heuristic search.

    I. POHL                                                         219

 13 A set-oriented property-structure representation

    for binary relations, SBP.  E.J.SANDEWALL                       237

 14 Rediscovering some problems of artificial intelligence in the

    context of organic chemistry.

    B.G. BUCHANAN, G.L. SUTHERLAND and E.A. FEIGENBAUM              253

 15 Memo functions, the graph Traverser and a simple control

    situation.  D.L. MARSH                                          281

 16 Experiments with the adaptive Graph Traverser.

    D. MICHIE and R. ROSS                                           301

 MAN-MACHINE INTERACTION

 17 An interactive theorem-proving program.

    J.R. ALLEN and D. LUCKHAM                                       321

 18 A symbol manipulation system.

    F.V. McBRIDE, D.J.T. MORRISON and R.M. PENGELLY                 337

 COGNITIVE PROCESSES: METHODS AND MODELS

 19 Associative memory models.

    D. WILLSHAW and H.C. LONGUET-HIGGINS                            351

 20 Hierarchical decomposition of complexity.  M.H. VAN EMDEN       361

 PATTERN RECOGNITION

 21 A grammar for the topological analysis of plane figures.

    P.BUNEMAN                                                       383

 22 Shape analysis by use of Walsh functions.  N.H. SEARLE          395

 23 Conic sections in automatic chromosome analysis.  K.X. PATON    411

 24 Centromere finding: some shape descriptions for small

    chromosome outlines.  D.RUTOVITZ                                435

 25 ESOTERIC II- an approach to practical voice control:

    progress report.  D.R. HILL and E.B. WACKER                     463

 26 On imitative systems theory and pattern recognition.

    P.A.V. HALL                                                     495

 PRINCIPLES FOR DESIGNING INTELLIGENT ROBOTS

 27 Planning and robots.  J.E. DORAN                                519

 28 Robotologic.  P.J. HAYES                                        533

 29 Design of low-cost equipment for cognitive robot research.

    H.G. BARROW and S.H. SALTER                                     555

 APPENDIX

    Bibliography on proving the correctness of computer programs.

    R.L. LONDON                                                     569

 INDEX                                                              581

Publisher: Edinburgh University Press